『Propositions as ［Types］』
Title: Propositions as [Types]
Year: 2004
1. どんなもの？
依存型理論に bracket types（ブラケット型／squash types） という新しい型構成子[A]を導入し、「型」と「命題」を区別しつつ結びつける理論を与えた論文。[A] は「A が inhabited である」という事実だけを表す命題型で、計算的内容はすべて消去される。これにより、依存型理論の内部で一階述語論理を自然に表現できることを示す。 Propositions=[Types]
$ Γ⊢p:[A],q:[A]⇒Γ⊢p=q:[A]
2. 先行研究と比べてどこがすごい？
Mendler の squash types や Maietti の mono types を統一的に整理し、「正則圏（regular categories）の内部言語がこの型理論に正確に対応する」という完全性定理を与えた点が新しい。 $ DTT+{1, Σ, Eq, []}
単なる構文的提案ではなく、圏論的意味論（image factorization）と厳密に対応づけた点が大きな貢献。
3. 技術や手法のキモはどこ？
bracket types [A] = 射 A → Γ の image という圏論的解釈
正則圏における regular epi–mono 分解 を用いた意味論
bracket を使って ∃ や ∨ を「型から命題へ落とす」翻訳を実現
4. どうやって有効だと検証した？
bracket types を含む依存型理論について正則圏に対する健全性（soundness）と完全性（completeness） を証明 構文的圏（syntactic category）を構成し、それが正則圏になることを示すことで、理論と意味論が一致することを保証
その結果として、一階論理との対応や保守性結果を導出
5. 議論はある？
完全性は すべての直観主義一階論理 ではなく、「left-stable」などの制限された断片に対して成立
bracket を ¬¬A と同一視できないモデルの存在など、古典論理との関係には注意が必要
6. 次に読むべき論文は？
[Men90] N. P. Mendler. Quotient types via coequalizers in Martin-Löf type theory. In G. Huet and G. Plotkin, editors, Informal Proceedings of the First Workshop on Logical Frameworks, Antibes, May 1990, pages 349–360, 1990.
[Mai98b] M.E. Maietti. The Type Theory of Categorical Universes. PhD thesis, Universit`a Degli Studi di Padova, 1998.
mono types を含む型理論と Heyting pretopos の内部言語の完全性を扱う。
[AG02] P. Aczel and N. Gambino. Collection principles in dependent type theory. In P. Callaghan, Z. Luo, J. McKinna, and R. Pollack, edi tors, Types for Proofs and Programs, International Workshop, TYPES 2000, Durham, UK, December 8-12, 2000, Selected Papers, volume 2277 of Lecture Notes in Computer Science, pages 1–23. Springer, 2002.
論理と型理論を分離した logic-enriched type theory の代表例。
[Pal04] E. Palmgren. A categorical version of the Brouwer-Heyting-Kolmogorov interpretation. Mathematical Structures in Computer Science, 14:57–72, 2004
image factorization と直観主義論理の関係を意味論的に論じた研究。